package ca.shojaei.mini_sat;
import ca.shojaei.mini_sat.Parser;
import ca.shojaei.mini_sat.Parser.ParseError;

import java.io.BufferedReader;
import java.io.Console;
import java.io.IOException;
import java.io.InputStreamReader;
import java.util.*;
import ca.shojaei.mini_sat.test.*;
/*import org.sat4j.*;
import org.sat4j.core.*;
import org.sat4j.minisat.*;
import org.sat4j.minisat.constraints.cnf.*;
import org.sat4j.opt.*;
import org.sat4j.specs.*;
*/

public class Main {
	

	/**
	 * @param args
	 * @throws IOException 
	 * @throws ParseError 
	 */
	public static void main(String[] args) throws IOException, ParseError {

		Vector<Test> tests = new Vector<Test>();

		/*tests.add(new TestItem());
		tests.add(new TestAnd());
		tests.add(new TestOr());
		tests.add(new TestExistNext());
		tests.add(new TestForAllNext());
		tests.add(new TestExsitsUntil());
		tests.add(new TestForAllUntil());
		tests.add(new TestReadFile());*/

		for(int i = 0; i < tests.size() ; i++)
		{
			if(!tests.get(i).runTest())
			{
				System.out.println("Test number " + i + " failed");
				return;
			}
		}

		System.out.println("All tests passed!");

		/// Over is reza's tests

		System.out.println("Let's get serious now, let's do some work.\n");	
		BufferedReader br;
		String ctl = "";

		Model1Solver solver = null;
		Model2Solver solver2 = null;

		System.out.print("Enter the Model you want to check (enter 1 or 2): ");
		br = new BufferedReader(new InputStreamReader(System.in));
		ctl = br.readLine();
		int model = Integer.parseInt(ctl);
		if(model == 1) {
			solver = new Model1Solver();
		}
		if(model == 2){
			System.out.print("Ok, then we need  starting state to check this model. \n " +
			"Please insert the path of the file containing the initial configuration.");
			br = new BufferedReader(new InputStreamReader(System.in));
			ctl = br.readLine();

			solver2 = new Model2Solver(ReadFile.getState(ctl));
		}



		Clause clause;

		while(!ctl.equals("#")){
			System.out.print("Enter the CTL to check: ");
			br = new BufferedReader(new InputStreamReader(System.in));
			ctl = br.readLine();
			if(ctl.equals("#")){
				System.out.println("Thank you, this assignment was interesting!");
				break;
			}
			clause = Parser.Parse(ctl);

			System.out.println("Printing: " + ctl);
			Parser.printClause(clause);
			System.out.println(" ");
			Parser.printTreeClause(clause);

			if(model == 1){
				if(solver.solve(clause))
					System.out.println("Yes!");
				else
					System.out.println("No");
			}
			if(model == 2){
				if(solver2.solve(clause))
					System.out.println("Yes!");
				else
					System.out.println("No");
			}
		}
	}
}		

/*
ISolver solver = SolverFactory.newDefault ();
// prepare the solver to accept MAXVAR variables . MANDATORY
solver.newVar(3);
// not mandatory for SAT solving . MANDATORY for MAXSAT solving
solver.setExpectedNumberOfClauses(NBCLAUSES);
// Feed the solver using Dimacs format , using arrays of int
// ( best option to avoid dependencies on SAT4J IVecInt )
//for ( int i =0; i < NBCLAUSES ;i ++) {
int [] clause1  = {1,3};
int [] clause2  = {-1,-3};
int [] clause3 = {-3, 1};
int [] clause4 = {3, -1};
int [] clause5 = {-3};
int [] clause6 = {-1};
	
try{
// get the clause from somewhere
// the clause should not contain a 0,
// only integer ( positive or negative )
// with absolute values less or equal to MAXVAR
// e.g. int [] clause = {1 , -3, 7}; is fine
// while int [] clause = {1 , -3, 7, 0}; is not fine
solver.addClause ( new VecInt ( clause1 )); // adapt Array to IVecInt
solver.addClause(new VecInt(clause2));
solver.addClause(new VecInt(clause3));
solver.addClause(new VecInt(clause4));
solver.addClause(new VecInt(clause5));
solver.addAllClauses()
//VecInt 

// we are done . Working now on the IProblem interface
IProblem problem = solver ;
if ( problem.isSatisfiable ()) {
	System.out.println("Staisfied");
	
}else {
    System.out.println("unsatisfied");   
}
}catch (Exception ex)
{
	System.out.println("Error: " + ex.getMessage());
}

*/